EqDecider($T$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$${\it eq}$:($T$$\rightarrow$$T$$\rightarrow\mathbb{B}$) $\times$ ($\forall$$x$:$T$, $y$:$T$. ($x$ = $y$ $\in$ $T$) $\Leftarrow\!\Rightarrow$ ($\uparrow$(${\it eq}$($x$,$y$))))